package kodkod.analysis.AST;

import java.util.*;
import kodkod.ast.BinaryExpression;
import kodkod.ast.BinaryFormula;
import kodkod.ast.BinaryIntExpression;
import kodkod.ast.ComparisonFormula;
import kodkod.ast.Comprehension;
import kodkod.ast.ConstantExpression;
import kodkod.ast.ConstantFormula;
import kodkod.ast.Decl;
import kodkod.ast.Decls;
import kodkod.ast.ExprToIntCast;
import kodkod.ast.Expression;
import kodkod.ast.Formula;
import kodkod.ast.IfExpression;
import kodkod.ast.IfIntExpression;
import kodkod.ast.IntComparisonFormula;
import kodkod.ast.IntConstant;
import kodkod.ast.IntExpression;
import kodkod.ast.IntToExprCast;
import kodkod.ast.LeafExpression;
import kodkod.ast.MultiplicityFormula;
import kodkod.ast.NaryExpression;
import kodkod.ast.NaryFormula;
import kodkod.ast.NaryIntExpression;
import kodkod.ast.Node;
import kodkod.ast.NotFormula;
import kodkod.ast.ProjectExpression;
import kodkod.ast.QuantifiedFormula;
import kodkod.ast.Relation;
import kodkod.ast.RelationPredicate;
import kodkod.ast.SumExpression;
import kodkod.ast.UnaryExpression;
import kodkod.ast.UnaryIntExpression;
import kodkod.ast.Variable;
import kodkod.ast.visitor.AbstractVoidVisitor;
import kodkod.ast.visitor.VoidVisitor;

public abstract class ExtendedVoidVisitor extends AbstractVoidVisitor {
	
	public void visit(Node node) {
		if (node instanceof Decls) {
			if (node instanceof Decl) {
				visit((Decl)node);
			} else {
				visit((Decls)node);
			}
		}
		else if (node instanceof Expression) {
			if (node instanceof BinaryExpression) {
				visit((BinaryExpression)node);
			}
			else if (node instanceof Comprehension) {
				visit((Comprehension)node);
			}
			else if (node instanceof IfExpression) {
				visit((IfExpression)node);
			}
			else if (node instanceof IntToExprCast) {
				visit((IntToExprCast)node);	
			}
			else if (node instanceof LeafExpression) {
				if (node instanceof ConstantExpression) {
					visit((ConstantExpression)node);
				}	
				else if (node instanceof Relation) {
					visit((Relation)node);
				}
				else if (node instanceof Variable) {
					visit((Variable)node);
				}
			}
			else if (node instanceof NaryExpression) {
				visit((NaryExpression)node);
			}
			else if (node instanceof ProjectExpression) {
				visit((ProjectExpression)node);
			}
			else if (node instanceof UnaryExpression) {
				visit((UnaryExpression)node);
			}
		}
		else if (node instanceof Formula) {
			if (node instanceof BinaryFormula) {
				visit((BinaryFormula)node);
			}
			else if (node instanceof ComparisonFormula) {
				visit((ComparisonFormula)node);
			}
			else if (node instanceof ConstantFormula) {
				visit((ConstantFormula)node);
			}
			else if (node instanceof IntComparisonFormula) {
				visit((IntComparisonFormula)node);
			}
			else if (node instanceof MultiplicityFormula) {
				visit((MultiplicityFormula)node);
			}
			else if (node instanceof NaryFormula) {
				visit((NaryFormula)node);
			}
			else if (node instanceof NotFormula) {
				visit((NotFormula)node);
			}
			else if (node instanceof QuantifiedFormula) {
				visit((QuantifiedFormula)node);
			}
			else if (node instanceof RelationPredicate) {
				visit((RelationPredicate)node);
			}
		}
		else if (node instanceof IntExpression) {
			if (node instanceof BinaryIntExpression) {
				visit((BinaryIntExpression)node);
			}
			else if (node instanceof ExprToIntCast) {
				visit((ExprToIntCast)node);
			}
			else if (node instanceof IfIntExpression) {
				visit((IfIntExpression)node);
			}
			else if (node instanceof IntConstant) {
				visit((IntConstant)node);
			}
			else if (node instanceof NaryIntExpression) {
				visit((NaryIntExpression)node);
			}
			else if (node instanceof SumExpression) {
				visit((SumExpression)node);
			}
			else if (node instanceof UnaryIntExpression) {
				visit((UnaryIntExpression)node);
			}
		}
	}
	
	protected String getNodeName(Node node) {
		if (node instanceof Decls) {
			return "Decl";
		}
		if (node instanceof Expression) {
			if (node instanceof UnaryExpression) {
				return ((UnaryExpression)node).op().toString();
			}
			if (node instanceof BinaryExpression) {
				return ((BinaryExpression)node).op().toString();
			}
			if (node instanceof NaryExpression) {
				return ((NaryExpression)node).op().toString();
			}
			if (node instanceof Comprehension) {
				return "{Comprehension}";
			}
			if (node instanceof IfExpression) {
				return "IfThenElse";
			}
			if (node instanceof ProjectExpression) {
				return "Projection";
			}
			if (node instanceof IntToExprCast) {
				return "CastToExp"+((IntToExprCast)node).op().name();
			}
			if (node instanceof LeafExpression) {
				if (node instanceof ConstantExpression) {
					return ((ConstantExpression)node).name();
				}
				if (node instanceof Relation) {
					return ((Relation)node).name();
				}
				if (node instanceof Variable) {
					return "$"+((Variable)node).name();
				}
			}
		}
		if (node instanceof Formula) {
			if (node instanceof IntComparisonFormula) {
				return ((IntComparisonFormula)node).op().toString();
			}
			if (node instanceof QuantifiedFormula) {
				return ((QuantifiedFormula)node).quantifier().toString();
			}
			if (node instanceof NaryFormula) {
				return ((NaryFormula)node).op().toString();
			}
			if (node instanceof BinaryFormula) {
				return ((BinaryFormula)node).op().toString();
			}
			if (node instanceof NotFormula) {
				return "NOT";
			}
			if (node instanceof ComparisonFormula) {
				return ((ComparisonFormula)node).op().toString();
			}
			if (node instanceof MultiplicityFormula) {
				return ((MultiplicityFormula)node).multiplicity().toString();
			}
			if (node instanceof RelationPredicate) {
				switch (((RelationPredicate)node).name()) {
				case FUNCTION :
					return "RP.Func";
				case TOTAL_ORDERING :
					return "RP.TotOrd";
				case ACYCLIC :
					return "RP.Acyc";
				default :
					return "UnspecifiedRelationPredicate";
				}
			}
			if (node instanceof ConstantFormula) {
				return ((ConstantFormula)node).toString();
			}
		}
		if (node instanceof IntExpression) {
			if (node instanceof ExprToIntCast) {
				return "CastToInt"+((ExprToIntCast)node).op().toString();
			}
			if (node instanceof NaryIntExpression) {
				return ((NaryIntExpression)node).op().toString();
			}
			if (node instanceof BinaryIntExpression) {
				return ((BinaryIntExpression)node).op().toString();
			}
			if (node instanceof UnaryIntExpression) {
				return ((UnaryIntExpression)node).op().toString();
			}
			if (node instanceof SumExpression) {
				return "SUM";
			}
			if (node instanceof IntConstant) {
				return ((IntConstant)node).toString();
			}
		}
		
		return "UnspecifiedNode";
	}
}
